The present invention relates generally to the field of functional verification of digital circuit designs. More specifically, the present invention relates to the field of formal verification of a digital circuit design and verifying the behavior of a circuit model to satisfy specified properties.
Recent increases in the complexity of modern integrated circuits have exacerbated the difficulty of verifying design correctness. The verification phase of a typical integrated circuit design project consumes approximately 70-80% of the total time and resources dedicated to a project. Flaws in the design that are not found during the verification phase have significant economic impact in terms of increased time-to-market and reduced profit margins.
A typical design flow for integrated circuit design includes many steps that proceed sequentially, with each step depending on the results of the previous steps. Consequently, when a flaw is discovered in a step, all the previous steps must be repeated, often at a significant cost. Hence, it is highly desirable to find and fix design flaws as early as possible in a design flow.
Traditionally, simulation-based techniques have been used to verify design correctness. Transistor-level simulation based techniques were used in the early 1970s and logic gate-level simulation based techniques were used in the late 1980s. As the complexity of designs increased with the passage of time, drawbacks associated with these techniques came into light. These techniques became less effective because of their inability to completely and quickly verify large designs. A popular alternative is the use of Register Transfer Language (RTL)-level simulation. Contemporary verification and debugging tools use various levels of abstractions for defining design specifications. These abstractions are expressed in high-level description languages. High-level description languages provide a number of functionalities for analyzing and verifying a design while performing simulation. For example, a designer can navigate the design hierarchy, view the RTL source code, and set breakpoints on a statement of an RTL source code to stop the simulation. Also, line numbers are provided in the RTL source code to identify different lines and statements. Further, the verification and debugging tools often support viewing and tracing variables and some times even signal values. These RTL-level simulation tools typically also offer these and other types of RTL debugging functionalities.
The verification tools as mentioned above typically follow a design flow. In the first step of the design flow, the conceptual nature of the integrated circuit is determined. The desired functionality of a circuit is expressed as a collection of properties or specifications, and possibly as a model of the behavior in a high-level language such as C++. The RTL model of the digital circuit is built based upon knowledge of the specifications or the high-level model. The RTL model is expressed in a hardware description language (HDL) such as Verilog or VHDL available from IEEE of New York, N.Y. Many other steps such as synthesis, timing optimization, clock tree insertion, place and route, etc., yield subsequent transformations of the design. These transformations eventually result in a set of masks that are fabricated into integrated circuits. The current invention is targeted at finding design flaws in the RTL model of the design, which is a very early phase of the design flow.
In the design flow, creation of RTL source code is followed by verification in order to check the compliance of the RTL source code to the design specifications. Three approaches commonly used to verify the design at the RTL level are simulation, emulation and formal methods.
Simulation is one of the most prevalent methods used to determine whether the design is in accordance with the specifications by simulating the behavior of the RTL model. The simulation process uses RTL source code and a “Testbench” to verify a design. The Testbench contains a subset of all possible inputs to the circuit/logic. For an ‘n’ input circuit, there are 2n possible input values at any given time. For large n, e.g., for a complex design, the number of possible input sequences becomes prohibitively large. To simplify this, only a subset of all possible input sequences is described in any given Testbench. An example of such a tool is SMV from Carnegie Mellon University, Pittsburgh, Pa. To simulate the RTL model, a Testbench must be created to provide appropriate input stimulus to the RTL model. Creating the Testbench is a time consuming process. The process of simulating the Testbench is also time consuming. Furthermore, it is effectively impossible to create enough test cases to completely verify that the specified properties of the design are true. This is because of the sheer number of possible input sequences, and also because it requires in-depth knowledge and tremendous creativity on the part of the Testbench creator to imagine the worst-case scenarios.
An increasingly popular alternative is to use formal methods to completely verify properties of a design. Formal methods use mathematical techniques to prove that a design property is either always true, or to provide an example scenario (referred to as a counterexample) demonstrating that the property is false. One category of tools using formal methods to verify properties are known as Model Checkers. An example of a conventional model checking tool is the Formal-Check tool from Cadence Design Systems, Inc. of Santa Clara, Calif.
Traditionally, simulation has been used to verify the functionality of a digital design in an ad-hoc manner. When simulation is used, progress is tracked by, for example: (1) the number of tests created (random, constrained random, or directed) to generate stimulus, (2) the percentage (%) of input space simulated (for example, in processors with instruction architecture), (3) the percentage of lines in the design description that have been exercised by tests, (4) the extent in which signal values are toggled by the tests, (5) the extent in which finite state machines transit from a specific state to another specific state as exercised by the tests, and (6) the % of items in the test plan have corresponding tests. To measure these items, a combination of the following techniques can be used: ‘code-coverage’, ‘line-coverage’, ‘branch-coverage’, ‘subexpression-coverage’, ‘state-coverage’, ‘arc coverage’, and ‘functional coverage’, for example.
When a design team starts to use formal verification, these metrics become less useful, because formal verification analyzes all possible legal sequences of inputs (subjected to constraints) and formal verification leads to an emphasis on the completeness of the set of requirements, whereas simulation concentrates on the stimulus generation (and simulation checkers are not analyzed for completeness). As a result, there is a need to define new metrics to measure progress in the use of formal verification to verify a digital design.
One such conventional system for measuring coverage on a design is the use of a cone of logic with respect to a property. For example, RuleBase: an Industry-Oriented Formal Verification Tool, Ilan Beer, Shoham Ben-David, Cindy Eisner, and Avner Landver, 33rd Design Automation Conference, DAC 1996, which is incorporated by reference herein in its entirety. In this paper, the authors identify the cone of logic as the relevant portion of the design with respect to a property and states that if the formula verifies a property of one design output, only this output and its input cone of logic are necessary. The RuleBase paper identifies unnecessary parts and removes them.”
Other references use a “cone of logic” to determine if more properties should be written. However, the use of analysis region (which is the same or smaller than the full cone of logic) to formally verify a property means that a coverage metric using the cone of logic does not provide a good indication of how many properties should be written to completely verify a block. On the other hand, in the present invention, because an analysis region should be tuned to be as small as possible to achieve a fast true proof, this provides a good balance between achieving complete analysis region coverage and achieving minimal analysis region for fast formal verification.
What is needed is a system and method for (1) measuring the progress of a formal verification process using the concept of an analysis region, (2) measuring the effectiveness of the current set of properties/requirements in verifying different portions of logic within the design and (3) having a visualization display that communicates the measurement succinctly to the user.